(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #x952a48e294e4e49a) #x952a48e294e4e49a))
(constraint (= (f #x5ab43ee73d72c6ae) #x05ab43ee73d72c6b))
(constraint (= (f #x5d96c533e698035c) #x05d96c533e698035))
(constraint (= (f #xde9c8b5540eee55d) #xde9c8b5540eee55e))
(constraint (= (f #xebad293d8d8c48e9) #xebad293d8d8c48ea))
(constraint (= (f #x412543d8ebed3da1) #x412543d8ebed3da2))
(constraint (= (f #x53bc547776d235e7) #x053bc547776d235e))
(constraint (= (f #xe85e4327868109c1) #xe85e4327868109c2))
(constraint (= (f #x198957ee7198626e) #x0198957ee7198627))
(constraint (= (f #x5bb21a9e12ed5ece) #x5bb21a9e12ed5ece))
(constraint (= (f #x70d6b0a3cb2698d3) #x70d6b0a3cb2698d4))
(constraint (= (f #xc384c6be2774cd82) #x0c384c6be2774cd8))
(constraint (= (f #x0e7e28026e4435d3) #x0e7e28026e4435d4))
(constraint (= (f #x050d817aa390e367) #x0050d817aa390e36))
(constraint (= (f #xe8d04a9ee98eaceb) #xe8d04a9ee98eacec))
(constraint (= (f #xd398a20e59de2e46) #x0d398a20e59de2e4))
(constraint (= (f #xc7a09ae860c5b1d8) #xc7a09ae860c5b1d8))
(constraint (= (f #xb45a4422eb508e7b) #x0b45a4422eb508e7))
(constraint (= (f #xe65b99a5a332eabd) #x0e65b99a5a332eab))
(constraint (= (f #x864b479295423971) #x864b479295423972))
(constraint (= (f #x5358d4e2b2b604e0) #x05358d4e2b2b604e))
(constraint (= (f #xaae8e7375e3c37ee) #x0aae8e7375e3c37f))
(constraint (= (f #x968ae0ba9cbe178b) #x0968ae0ba9cbe178))
(constraint (= (f #xe921dd7a8e082d2d) #xe921dd7a8e082d2e))
(constraint (= (f #x47e211c8c80a0c94) #x47e211c8c80a0c94))
(constraint (= (f #x4120cca5ec5da48e) #x04120cca5ec5da49))
(constraint (= (f #x787a6e6a99bb95da) #x0787a6e6a99bb95d))
(constraint (= (f #x2cd6c8bbbda50ca0) #x2cd6c8bbbda50ca0))
(constraint (= (f #xd4949279c9743eba) #x0d4949279c9743eb))
(constraint (= (f #xc8eca63987382464) #x0c8eca6398738246))
(constraint (= (f #x989ee881d3778a5e) #x0989ee881d3778a6))
(constraint (= (f #xced8eaee8ee32ee3) #xced8eaee8ee32ee4))
(constraint (= (f #xea211b8e984b9948) #xea211b8e984b9948))
(constraint (= (f #xe847e0e7dcc3d607) #xe847e0e7dcc3d608))
(constraint (= (f #x913e50b3e732a9e7) #x0913e50b3e732a9e))
(constraint (= (f #x0e8edc116db22d99) #x00e8edc116db22d9))
(constraint (= (f #x8e0a401b61b4e448) #x08e0a401b61b4e44))
(constraint (= (f #x3378d092966e4883) #x3378d092966e4884))
(constraint (= (f #xeed58dece92c191c) #xeed58dece92c191c))
(constraint (= (f #xdd229c16b48db155) #xdd229c16b48db156))
(constraint (= (f #xa63a866b5e3c9ee2) #x0a63a866b5e3c9ee))
(constraint (= (f #x84556713c4b9084e) #x084556713c4b9085))
(constraint (= (f #xd45e8de41b326a0c) #x0d45e8de41b326a0))
(constraint (= (f #x06be2c8c97d04a1e) #x006be2c8c97d04a2))
(constraint (= (f #x56e79c6a94876968) #x56e79c6a94876968))
(constraint (= (f #x3ba4ee44c4910469) #x03ba4ee44c491046))
(constraint (= (f #x632e20ca35627e34) #x632e20ca35627e34))
(constraint (= (f #xa426b0ae9803273c) #xa426b0ae9803273c))
(constraint (= (f #x380ac2052c67ced6) #x380ac2052c67ced6))
(constraint (= (f #xbb36b6c9e7a7a6a7) #xbb36b6c9e7a7a6a8))
(constraint (= (f #x6023d9ee9c63d741) #x6023d9ee9c63d742))
(constraint (= (f #xa384e9bccc4490a4) #xa384e9bccc4490a4))
(constraint (= (f #xcd9d5d065e206226) #xcd9d5d065e206226))
(constraint (= (f #x4ae9b44d8d08e324) #x4ae9b44d8d08e324))
(constraint (= (f #x42917e0344b6dcce) #x042917e0344b6dcd))
(constraint (= (f #x85c8c052ae5574b6) #x085c8c052ae5574b))
(constraint (= (f #x2d23cbaee7e624ee) #x2d23cbaee7e624ee))
(constraint (= (f #x730822aeae653b53) #x730822aeae653b54))
(constraint (= (f #x14268d1ce0bad57b) #x014268d1ce0bad57))
(constraint (= (f #xe6e11e8c04202dd5) #xe6e11e8c04202dd6))
(constraint (= (f #x845bbed8e75154ed) #x0845bbed8e75154e))
(constraint (= (f #xde046ea673d69e3d) #x0de046ea673d69e3))
(constraint (= (f #xd7692b9083c95a26) #xd7692b9083c95a26))
(constraint (= (f #x93e959c7a211b9e4) #x093e959c7a211b9e))
(constraint (= (f #x0eeb0eee7b427dba) #x0eeb0eee7b427dba))
(constraint (= (f #x578d6099541652cd) #x0578d6099541652c))
(constraint (= (f #x519e6d2be40e652a) #x519e6d2be40e652a))
(constraint (= (f #x55a6a6e774282e81) #x55a6a6e774282e82))
(constraint (= (f #x2e5b499c79b5dc7c) #x02e5b499c79b5dc7))
(constraint (= (f #x744ab5c21c6ad47b) #x744ab5c21c6ad47c))
(constraint (= (f #xe4c13e726157252b) #x0e4c13e726157252))
(constraint (= (f #xa9e2629656889989) #xa9e262965688998a))
(constraint (= (f #x77579427dee939ee) #x77579427dee939ee))
(constraint (= (f #xee1023a8bbeee3ce) #xee1023a8bbeee3ce))
(constraint (= (f #x587e436b343944e1) #x0587e436b343944e))
(constraint (= (f #xce560e060e020d69) #xce560e060e020d6a))
(constraint (= (f #x21ac1ac75c192419) #x021ac1ac75c19241))
(constraint (= (f #x0e5dd0cb1bd72e7a) #x00e5dd0cb1bd72e7))
(constraint (= (f #x2b61936e30784279) #x02b61936e3078427))
(constraint (= (f #x72bad9b73ae9d178) #x72bad9b73ae9d178))
(constraint (= (f #x3a546124edee4631) #x3a546124edee4632))
(constraint (= (f #x19aae44e604eb2b1) #x19aae44e604eb2b2))
(constraint (= (f #x8c949d537a42777e) #x8c949d537a42777e))
(constraint (= (f #xe60bb206c8b6c585) #x0e60bb206c8b6c58))
(constraint (= (f #x2de90b0d7cb560e5) #x02de90b0d7cb560e))
(constraint (= (f #x055ee7c034b49eee) #x0055ee7c034b49ef))
(constraint (= (f #xd40e7b7e08e05ecc) #xd40e7b7e08e05ecc))
(constraint (= (f #xdced66775b5e958c) #x0dced66775b5e958))
(constraint (= (f #x73e7627ba488561e) #x73e7627ba488561e))
(constraint (= (f #x87404ab8b9e0784d) #x87404ab8b9e0784e))
(constraint (= (f #x8e66353a24e61391) #x8e66353a24e61392))
(constraint (= (f #x02748198a62ddb20) #x02748198a62ddb20))
(constraint (= (f #x20e855cc29a47c8e) #x20e855cc29a47c8e))
(constraint (= (f #x293ae587acb72192) #x0293ae587acb7219))
(constraint (= (f #x8e54bd72ace820aa) #x8e54bd72ace820aa))
(constraint (= (f #x9e7e720196e0c4b8) #x9e7e720196e0c4b8))
(constraint (= (f #x814e14ea9a2da656) #x814e14ea9a2da656))
(constraint (= (f #x5edac13c04bb54e6) #x05edac13c04bb54e))
(constraint (= (f #x7b0e2d0c1d7ec262) #x07b0e2d0c1d7ec26))
(constraint (= (f #x5e2000ae8b9d93ce) #x05e2000ae8b9d93d))
(check-synth)
(define-fun f_1 ((x (BitVec 64))) (BitVec 64) (ite (= (bvor #x0000000000000001 x) x) (ite (= (bvsrem x #x0000000000000009) #x0000000000000000) (bvneg (bvnot x)) (ite (= (bvand #x000000000000000c x) #x0000000000000000) (ite (= (bvurem x #x0000000000000005) #x0000000000000000) (ite (= (bvor #x0000000000000010 x) x) (bvneg (bvnot x)) (bvudiv x #x0000000000000010)) (bvneg (bvnot x))) (ite (= (bvashr x x) #x0000000000000000) (ite (= (bvor #x000000000000000a x) x) (ite (= (bvurem x #x0000000000000009) #x0000000000000001) (bvudiv x #x0000000000000010) (bvneg (bvnot x))) (bvudiv x #x0000000000000010)) (ite (= (bvand #x0000000000000006 x) #x0000000000000000) (bvneg (bvnot x)) (ite (= (bvsrem x #x000000000000000b) #x0000000000000000) (bvneg (bvnot x)) (ite (= (bvor #x0000000000000010 x) x) (bvudiv x #x0000000000000010) (ite (= (bvurem x #x000000000000000b) #x0000000000000001) (bvneg (bvnot x)) (ite (= (bvor #x000000000000000c x) x) (ite (= (bvurem x #x0000000000000007) #x0000000000000001) (bvudiv x #x0000000000000010) (bvneg (bvnot x))) (bvudiv x #x0000000000000010))))))))) (ite (= (bvor #x000000000000000e x) x) (ite (= (bvor #x0000000000000010 x) x) (ite (= (bvurem x #x0000000000000006) #x0000000000000000) (bvxor (bvudiv x #x0000000000000010) #x0000000000000003) x) (ite (= (bvsrem x #x0000000000000005) #x0000000000000000) (bvxor (bvudiv x #x0000000000000010) #x0000000000000001) (ite (= (bvurem x #x0000000000000007) #x0000000000000001) x (ite (= (bvurem x #x0000000000000009) #x0000000000000001) x (ite (= (bvurem x #x0000000000000003) #x0000000000000001) (bvxor (bvudiv x #x0000000000000010) #x0000000000000001) (ite (= (bvurem x #x0000000000000005) #x0000000000000001) (bvxor (bvudiv x #x0000000000000010) #x0000000000000001) x)))))) (ite (= (bvurem x #x000000000000000b) #x0000000000000000) (ite (= (bvurem x #x0000000000000007) #x0000000000000001) x (bvudiv x #x0000000000000010)) (ite (= (bvsrem x #x0000000000000007) #x0000000000000000) x (ite (= (bvurem x #x000000000000000c) #x0000000000000000) (ite (= (bvor #x0000000000000010 x) x) (bvxor (bvurem x #x000000000000000c) x) (ite (= (bvurem x #x0000000000000007) #x0000000000000001) (bvxor (bvurem x #x000000000000000c) x) (ite (= (bvurem x #x0000000000000005) #x0000000000000001) (bvxor (bvurem x #x000000000000000c) x) (bvudiv x #x0000000000000010)))) (ite (= (bvurem x #x0000000000000007) #x0000000000000001) (bvudiv x #x0000000000000010) (ite (= (bvurem x #x000000000000000e) #x0000000000000000) (bvudiv x #x0000000000000010) (ite (= (bvor #x000000000000000c x) x) (bvudiv x #x0000000000000010) (ite (= (bvsrem x #x000000000000000b) #x0000000000000000) (bvudiv x #x0000000000000010) (ite (= (bvurem x #x0000000000000003) #x0000000000000001) (ite (= (bvand #x0000000000000004 x) #x0000000000000000) (ite (= (bvand #x0000000000000002 x) #x0000000000000000) x (ite (= (bvurem x #x0000000000000005) #x0000000000000000) x (bvudiv x #x0000000000000010))) x) x)))))))))))
